.device xgp;
.if xcribl then pagehigh ← 56
.else
.pagehigh ← 53;
.if xcribl then pagewide ← 82
.else
.pagewide ← 69;
.page frame pagehigh high pagewide wide;
.area heading line 1 to 3
.area text line 4 to pagehigh-3
.area footing line pagehigh-2 to pagehigh
.place text
.turn on "%","{","α","\"
.EVENLEFTBORDER←ODDLEFTBORDER←1000
.
.if xcribl then start
.font 1 "foll30[fnt,rww]"	;comment   main text;
.font 2 "foli30[fnt,rww]"	;comment   italics;
.font 3 "folb30[fnt,rww]"	;comment   boldface subtitle headings;
.font 4 "ngr30"	;comment   boldface subtitle headings;
.font a "beeSIx"	;comment   boldface subtitle headings;
.end
.if xcribl then start
.AT "ffi" ⊂ IF THISFONT ≤ 3 THEN "β" ELSE "fαfαi" ⊃;
.AT "ffl" ⊂ IF THISFONT ≤ 3 THEN "αα" ELSE "fαfαl" ⊃;
.AT "ff" ⊂ IF THISFONT ≤ 3 THEN "π" ELSE "fαf" ⊃;
.AT "fl" ⊂ IF THISFONT ≤ 3 THEN "∂" ELSE "fαl" ⊃;
.AT "fi" ⊂ IF THISFONT ≤ 3 THEN "λ" ELSE "fαi" ⊃;
.		end
.single space
.macro chk ⊂ if lines ≤4 then next page ⊃
.
.count chap inline from 1 to 9 printing "! 1";
.count sec  inline from 1 to 9 in chap printing "!.1";
.macro CHAPTER(foo)⊂
.chapname ← "foo";skip 2
.once flush left ; select 3
Section {next chap;chap!}      foo
.send contents ⊂

Section {chap!} foo∞ ∞.→ {page}
.	⊃
.	skip ⊃
.
.macro sect(foo)⊂
.	skip 2 ; chk; once flush left ; select 3
Subsection {next sec;sec!}      foo
.send contents ⊂

                 {sec!} foo∞ ∞.→ {page}
.⊃
.	skip ⊃
.macro table ⊂ begin indent 8,16, 8;select 2;tabs 17,25; ⊃;
.
.
.comment  makes table of contents;
.
.macro tabcon ⊂
.	portion contents
.	chapname← "Table of Contents"
.	count page printing "i"
.	next page
.	nofill nojust
.	place text
.	indent 0,30,10
.	select 4
.	once center
CONTENTS
.       skip 3
.	turn on "∞→"
.	receive 
.	turn off "∞→"
.		⊃
.begin center
.skip 12
.select a
FOLMRG
.skip 2
A program for formating FOL proofs
.skip
Robert Filman
      {date}
.end
.insert contents 
.portion mainportion
.count page to 999
.
.chapname ← "Introduction"
.EVERY  HEADING (FOLMRG,,{DATE})
.EVERY FOOTING (,{PAGE},)
.next page
.tabbreak
.indent 0
.chapter(FOLMRG)
.select 3
	FOLMRG is a program for reformating FOL input and output files.
It has the ability to justify proofs, count statements, prepare
for pub output, and rename identifiers.
.select 1

	The program usually expects two input files: a FOL command
file, and a file created by a SHOW PROOF on the proof that command file
generated.  It generates a reformatted output file.  The reformatting
is controled by the settings of several
switches.  The switches and their meanings are described in the latter
sections of this document.  
	For the novice user, there are also several modes.
Selection of a mode automatically selects a convenient and related
group of switches.
	It is possible to run FOLMRG on a single input file, rather
than a pair of files.  This is particularly useful for reformatting
a PROOF file only, or for using FOLMRG to rename the identifiers
in any file.
.chapter MODES
	When execution of the program begins, the user is confronted
with a choice of modes.  Selection of a mode sets some switches;
more switches can be added later.
	The user wishing a fast and dirty pub preparation can
merely request one of the PUB modes, express no desire to set other switches,
and proceed to tell FOLMRG which files to process.

	There are currently four modes

.table;
%3F%*\FOL mode.  Proof is printed in medium size type.
Different fonts are used for FOL commands and responses.
A header is printed in the file with PUB declarations.
Equivalent to requesting switches:
M,E,H,JF=70,U,B,X,C=α%6,R=α%7.
The resulting file is ready for PUB.

%3A%*\FOL appendix mode.  Smaller type, but, then again, you
get more to the page.  Appropriate header is printed.
Acts like switches:
M,E,H,JF=108,U,B,X.
The resulting file is ready for PUB.

%3C%*\Two column mode.  Like appendix mode, but with a narrower
column width.  The appropriate pub commands are given to obtain
two column output.  Gives switches:
M,E,H,JF=50,U,B,X.
The resulting file is ready for PUB.

%3P%*\Proof file only.  When you want to reformat a file created
by FOLs SHOW PROOF command.  Lets you get a different
linelength, rename variables, or, collect frequency statistics
on the different FOL commands you used.
Gets the switches
Z=,Y=,I

%3R%*\Renaming only.  When you want to use this program to
do renamings of the identifiers in a file.  Works on non-fol
files, too.
.end

	If one of the PUB modes is requested, the users line editor is loaded
with a request to pub after program execution.  Any letter other than F,A,P or R
is ignored.  In any case, you're asked if you want to set any other switches.

	The headers produced by the F and A options are, respectively,
the files FOLMAC.DAT[MRG,REF] and APPMAC.DAT[MRG,REF].
.chapter SWITCHES
	The are several classes of switches.  Successive sections describe the
switches in each class.
.sect (|File control Switches F,T,P|)

	Certain switches control where to commence and terminate reading
files.
.table;
%3F=%4λ%2\fetch From mark %4λ%*.  Start processing the FOL file when the statement
MARK  %4λ%*; is encountered.  %4λ%* can be, of course, any FOL token.

%3T=%4λ%2\fetch To mark %4λ%*.  Stop program processing when the mark %4λ%* is reached.
.end

An alternate way of skiping part of a file involves the P switches

.table
%3PF=n%*\start reading Fol file at Page n

%3PP=n%*\start reading Proof file at Page n
.end
.sect(|Input control switches  G,Y,M,E,D,V,X,I,N,SP|)

Several switches control processing of the FOL file input.  The switches
request certain conversions of and deletions from the input stream.

The first four switches in this group request the deletion or inclusion
of certain characters from the FOL input file.
.table
%3M%*\Print the Marks in the FOL input file.  If M is not set,
then MARK commands in the input file are not transfered to the output
file.

%3E%*\Print the declarative and administrative commands in file.
Same as M, except for declares, shows, attachments, mg, etc.

%3D%*\Delete all comments.  Both kind of comments (COMMENT and α%)
are recognized.  If this switch is not requested, comments will
be put in the output file.

%3V%*\Don't print formfeeds seen in the FOL file.  Otherwise, the program
will convert any formfeed in the FOL input file to an appropriate
formfeed on output.  The program will avoid spliting a single
command onto two different pages, however.
.end

The next set of switches request certain conversions be done on the input
files before further processing.
.table
%3X%*\All tabs are converted to the character `α\'.  Additionally,
all `α\'s already in the file are PUB quoted.  Note that if you
specify a set of PUB quote characters after invoking the X
switch (Q switch), then α\ will not necessarily be quoted.

%3YA=file%*\Do the renamings requested in `file'

%3YO=file%*\Do the renamings requested in `file'.  Do no other processing.
The Y switches are used for renaming the identifiers in a file.
The argument file has a list of identifier changes, one
per line, the first the old word, the second, its replacement.
The two words are separated by a space.  Substitution pairs
must exist one per line.  Formfeeds are ignored on input, but
the file may contain no other information (such as blank lines
or ETV directory pages).  Using a Y option slows the program
to about 40α% of its original speed.  If the YO option is requested,
no other switches are considered, the program merely does identifier
substitution.  However, the input file is no longer assumed to
be a FOL input file; any file may be used.  Hence, FOLMRG may
be used as a general identifier substitution program.
.end

Other input selection switches.
.table
%3I%*\Formatting only one input file.  If you want to take a proof
file, and process it with the other options, (that is, treat the
FOL generated commands as coming from the file), use the I option.
You will be asked for only one input file.

%3N%*\Assumptions involving Ntuples are made (so <> are not relationals)
FOLMRG does not look at/know about the declarations made in the
FOL proof.  Not knowing the types of identifiers implies an ambiguity
in determining the number of statements generated by a single fol
command.  To wit, ASSUME A < B , C >; might generate either a
single line refering to the action of the prefix predicate A
when confronted with the tuple argument <B,C>, or it might
generate the two proof steps, A<B, and C>, where > is then obviously
an individual.  The default is the former, but if your declarations
are obscure enough, you might appreciate the latter.  If none
of this makes sense to you, you probably don't need the N switch.

%3G%*\If you find a fetch command, Get that file, & transcribe it verbatim
This switch doesn't exactly act this way.  In fact, it hasn't yet been
implemented.  If anybody really wants it, however, I might find the
time to implement full processing of fetch commands.
.end

One switch controls the formatting of the proof input file, the SP switch.
.table
%3SP=n%*\n is the number of lines between the FOL command and the proof step
in the proof input file.  The default is one, and, if you're just
reading a file that FOL created, you can leave this switch alone.
Setting it is useful for re-formatting a file that FOLMRG has formatted
already.
.end
.sect(|Output formatting switches H,Q,A,O,S,J,U,B,C,R,Z|)

These switches detail the reformating actions

In step changes.
.table
%3A=c%*\PUB quote character is to be (default = %4αα%*)(Alpha character)
Whenever FOLMRG has to quote a PUB command character, it uses c.

%3Q=s%*\Makes the set of PUB quote chars to s (default = %4ααα%α{%2 )
Whenever one of the PUB quote characters is encountered in output
stream, it is quoted with the pub quote character.  This does
not include, of course, pub command characters inserted by FOLMRG

%3O%*\Don't quote periods in column One
Unless the O option is invoked, FOLMRG will
PUB quote (alphachar) every period in column one.


%3Z=s%*\Print Ztring s before every command (default=`*****')

%3C=α%c%*\Switch to font c in Commands (default NULL)

%3R=α%d%*\Switch to font d in Responses (default NULL) (α% is font switch char)

\Every line of command from the FOL file is surrounded on output,
by three strings.  The string s, followed by the characters α%c,
proceed each line.  The characters α%d end the line.  The s string
is abbreviated to its first character on all lines of a FOL
command other than the first.  This permits switching to another 
font for the FOL commands.
.END
 
Justification switches
.table
%3JFα{=n}%*\Do simple α% justifying, of lines of length n (JustFill)

%3JUα{=n}%*\Do complex justifying (don't split identifiers) (JUstify)

\FOLMRG knows of two ways to justify the proof output.
Either every line can be forced to the same length (JF),
which involves spliting identifiers and sticking percent
signs at the end of every line (this is the way the stuff
looks when it comes out of FOL), or the program can keep
your identifiers together on the same line.  This results in
a ragged right margin, but virtually no percent characters.
In either case, n is the length of the longest of the 
resulting lines.  If the =n is omitted, 108 is used for the
linelength.  Don't try asking for a linelength of less than 5;
it won't work.

%3U%*\JUstify the FOL commands, too.  FOLMRG will not remove
the interior CRLF's from FOL commands, but if a line of
FOL input is longer than linelength, using the U switch will
break it.
.end

Output spacing
.table
%3H%*\Keep commands & steps togetHer on the same page
Puts PUB %1GROUP%* and %1APART%* commands around rules of inference
and their generated steps.  Also around axiom definitions.

%3SA=n%*\Number of lines to Skip between command and answer (default = 0)(intrA)

%3SR=n%*\Number of lines to Skip between proof steps (default = 1)(inteR)

%3SW=n%*\Insert an additional blank line every n steps (default =10E6)(Skip When)

%3SF=n%*\Insert an additional page mark every n steps (default =10E6)(Skip When)

\The skip switches control the regular insertions of blank lines
in the output.  SA blank lines are inserted between a command and its
response, SR between the proof steps.  An additional blank line
is inserted every SW steps, and a formfeed, every SF steps.

%3B%*\Print α# in every Blank line.  also, add α# to the PUB quoted chars.
The B switch controls what is printed on blank lines.  If B
is invoked, then every blank line contains the PUB space character,
%1α#%*.  Every α# in the text is pub quoted.  Because of a PUB "feature",
invoking the B switch will pub more lines on each XGP output page.
.end
.sect(|Run time messages, and counters  L,W,K|)

Run time messages.
.table
%3L%*\Don't print line numbers of statements processed.
Unless you invoke the L switch, FOLMRG will print the line number
of each proof step it processes.  If you tired of having your
screen filled with little digits, try L.

%3W%*\Don't Warn me.
FOLMRG tries to warn you if certain unusual conditions occur.
Particularly, unterminated comments, and FOL commands that
do not match the proof file command provoke messages.  If you
don't want these messages, use the W switch.
.end

Counters
.table
%3K%*\Kount the FOL command frequency
FOLMRG has a facility for counting the frequency of the
FOL commands in your proof.  If you use the K switch, you
will be asked for a file for the results.
FOLMRG knows the state of the current FOL commands from the
information in HASH.DAT[MRG,REF].  Don't change this file
unless you know what you're doing.
.end
.chapter FILES
	FOLMRG will normally ask for the names of three files,
a FOL commands input file, a PROOF input file, and an OUTPUT file.
If the K switch is invoked, a file name for counter output is also
requested.   A Y option likewise requires the name of a data file.
If the I switch is called, FOLMRG requests only one primary input file.

	If the first file request is answered <filename>.*, then
the input files are presumed to be:
.begin nofill;select 2;indent 8,8,8;skip
FOL command file\<filename>.FOL
shown PROOF file\<filename>.PRF
primary output file\<filename>.OUT
file for counters\<filename>.KNT
.end
	Note that you cannot respond  FOOBAZ.*[FOO,BAZ]
.chapter Sample Run
.begin nofill


α.%2R FOLMRG%*
<display>
MODE?%2p%*
<display is cleared>

Do you want to set any of the switches yourself?%2y%*
<display>

Switches?%2T=MARKEND,jf=50,u,b,x,r=α%7,z=?????,k%*
<display is cleared>
FOL input file? %2FOOBAZ.FOL%*
PROOF input file? %2BAZFOO.PRF%*
Output file? %2PUTOUT.OUT%*

1 2 3 4 5 6 7  File for counters? %2CUMQAT.KNT%*
Finished

End of SAIL execution.
.end
.TABCON